package com.googlecode.kipler.satisfiability.interpolation.rule;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.syntax.concept.BooleanConcept;
import com.googlecode.kipler.syntax.concept.BooleanConcept.Constructor;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;

public class UnionInterpolantRule extends InterpolantRule {

	@Override
	public ConceptAssertion apply() {
		BasicWcsInterpolationData wcsData = (BasicWcsInterpolationData) getWcs()
				.getData();
		LabelManager labelMan = wcsData.getLabelManager();
		Formula condition = getCondition().iterator().next();
		Iterator<ConceptAssertion> prevIntIter = getPreviousInterpolants()
				.iterator();
		ConceptAssertion int1 = prevIntIter.next();
		ConceptAssertion int2 = prevIntIter.next();
		ConceptAssertion result = null;
		if (labelMan.isLeftDerived(condition)) {
			result = new ConceptAssertion(new BooleanConcept(Constructor.UNION,
					int1.getConcept(), int2.getConcept()), int1.getName());
		} else {
			result = new ConceptAssertion(new BooleanConcept(
					Constructor.INTERSECTION, int1.getConcept(), int2
							.getConcept()), int1.getName());
		}
		return result;
	}

}
